Alright, here we go.

This seems louder than earlier.

Never mind.

First things first, you might have noticed that I'm not Professor Kohlhase.

That's because Professor Kohlhase is not here today.

Instead you'll have to do with me.

My name is Dennis Müller.

I'm a postdoc in Professor Kohlhase's group.

Yeah, so much for that.

I have been told, and I hope that is correct, that we are squarely in the topic of propositional

logic, more precisely natural deduction calculus.

I'm going to do a very quick recap just so that we can all agree on what the hell we're

even talking about.

So, propositional logic, every logic ultimately consists of at least two things.

The first being a syntax.

A syntax is nothing but a simple grammar.

It tells us when strings of symbols are actually well-formed propositions of whatever logic

we are currently investigating, in this particular case, propositional logic.

So the syntax of propositional logic is straightforward.

We have either propositional variables or we have one of those connectives applied to

sub-formula, i.e.

conjunction, negation, disjunction, implications, equivalences.

If you want to, you can add the usual suspects, xor, xand, and all these kinds of things.

And that gives us a set of well-formed propositions, which so far mean nothing.

All we know is, is this a well-formed sentence or not?

If we want them to actually mean something, we need semantics, meaning we have to define

what a model for that particular language is.

For propositional logic, a model is literally just an assignment of propositional variables

to truth values, i.e. either true or false.

And if we have such an assignment for the propositional variables, then we can also

give interpretations for all of the connectives, i.e.

negations, disjunctions, and so on and so forth.

And then we can assign actual truth values to arbitrary propositions of our language.

If you want to actually do that, here is a nice example.

So given one of those formulas, you can now compute what the truth value of such a formula

is, and then you just step down through the entire syntax tree of that proposition.

Okay, so that red dot does not do much, but okay.

You can step through the entire syntax tree of your proposition and basically just insert

an i around every single letter in your formula, and then at the end you get something like

true or false.

So at that point you might question, why the hell are we even doing this?

This is literally just Boolean functions, the good old Boolean functions you all know

from any arbitrary programming language, right?

We have conjunction, i.e. ampersand, ampersand, we have negation, i.e. exclamation point,

and all these kinds of things.

The reason why we're doing this is twofold.

Reason number one, if we were to just talk about Boolean functions, then we can answer

exactly this kind of question, given an assignment of all the variables, i.e. given a bunch of

inputs, what is the output of my Boolean function?

But we are also going to be interested in much more complicated questions such as, given